00100	
00200	
00300	(DEFPROP ANCESTRY 
00400	 (LAMBDA(LLST)
00500	  (PROG (SPINE CAND FP Z)
00550	(SETQ CNT (ADD1(LENGTH CLAUSES)))
00600		(SETQ Z LLST)
00700	   C    (COND ((MEMBER (CDAR Z) SUPPORT) (SETQ SPINE (CONS (CAR Z) SPINE))))
00800		(SETQ Z (CDR Z))
00900		(COND (Z (GO C)))
01000		(SETQ CAND LLST)
01100	   A    (SETQ Z (RESEM (CAR SPINE) CAND))
01200		(COND ((NULL Z) (GO B)))
01300		(SETQ FP (CONS (CONS  SPINE CAND) FP))
01400		(SETQ SPINE Z)
01500		(SETQ CAND (CHOICE1 (CAR Z) LLST))
01600		(GO A)
01700	   B    (SETQ SPINE (CDR SPINE))
01800		(COND (SPINE (GO A)) ((NULL FP) (ERR (QUOTE NOPROOF))))
01900		(SETQ SPINE (CAAR FP))
02000		(SETQ CAND (CDAR FP))
02100		(SETQ FP (CDR FP))
02200		(GO B))) 
02300	EXPR)
02400	
02500	(DEFPROP RESEM 
02600	 (LAMBDA(C S)
02700	  (PROG (RES S1 R)
02800	   A    (COND ((NOT (HERE C)) (RETURN RES)))
02900		(SETQ S1 (CAR S))
03000		(COND ((NOT (HERE S1)) (GO B))
03100		      ((AND (ALLPOS C) (ALLPOS S1)) (GO B))
03200		      ((AND (ALLNEG C) (ALLNEG S1)) (GO B)))
03250	(COND((NOT(OR(ALLPOS C)(ALLPOS S1)))(GO B)))
03300		(SETQ R (RESOLVE C S1))
03400		(COND ((NULL R) (GO B)) ((MEMQ NIL R) (PROOF C S1) (ERR (QUOTE (QED)))))
03500		(SETQ RES (APPEND (FINI CLAUSES R C S1 EE1) RES))
03550	(SETQ CNT(PLUS CNT(LENGTH RES)))
03600	   B    (SETQ S (CDR S))
03700		(COND ((TTYIN) (UPDATE CLAUSES)))
03800		(COND (S (GO A)))
03900		(RETURN RES))) 
04000	EXPR)
04100	
04200	(DEFPROP FINI 
04300	 (LAMBDA(U R Z1 Z2 E)
04400	  (PROG (Z)
04500		(COND (UFLG (SETQ R (UNITREDUCT R UNAXP UNAXN))))
04600		(COND ((NULL R) (RETURN NIL)) ((NULL (CAR R)) (PROOF Z1 Z2) (ERR (QUOTE (QED)))))
04700		(SETQ COUNT (PLUS COUNT (LENGTH R)))
04800		(SETQ R (EDIT U R))
04900		(CLAUSES2 R)
05000		(COND ((NULL R) (RETURN NIL)))
05100		(BAKSUB CLAUSES R)
05200		(BOOKEEP E R (CONS Z1 Z2))
05300		(SETQ Z (UNITPN R))
05400		(SETQ UNAXP (APPEND (CAR Z) UNAXP))
05500		(SETQ UNAXN (APPEND (CDR Z) UNAXN))
05600		(RETURN R))) 
05700	EXPR)